1 /-
2 Copyright (c) 2019 Kenny Lau. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Kenny Lau
5
6 Adjoining elements to form subalgebras.
7 -/
8
9 import ring_theory.algebra_operations ring_theory.polynomial ring_theory.principal_ideal_domain
src └────────────────────────────┘ └────────────────────┘ └────────────────────────────────┘
10 import algebra.pointwise
src └───────────────┘
11
12 universes u v w
13
14 open lattice submodule ring
15
16 namespace algebra
17
18 variables {R : Type u} {A : Type v}
19 variables [comm_ring R] [comm_ring A]
20 variables [algebra R A] {s t : set A}
id └─┘
src └─┘
typ └─┘
21
22 theorem subset_adjoin : s ⊆ adjoin R s :=
23 set.subset.trans (set.subset_union_right _ _) subset_closure
24
25 theorem adjoin_le {S : subalgebra R A} (H : s ⊆ S) : adjoin R s ≤ S :=
26 closure_subset $ set.union_subset S.3 H
27
28 theorem adjoin_le_iff {S : subalgebra R A} : adjoin R s ≤ S ↔ s ⊆ S:=
29 ⟨set.subset.trans subset_adjoin, adjoin_le⟩
30
31 theorem adjoin_mono (H : s ⊆ t) : adjoin R s ≤ adjoin R t :=
32 closure_subset (set.subset.trans (set.union_subset_union_right _ H) subset_closure)
33
34 variables (R A)
35 @[simp] theorem adjoin_empty : adjoin R (∅ : set A) = ⊥ :=
doc └──┘
36 eq_bot_iff.2 $ adjoin_le $ set.empty_subset _
37 variables {A}
38
39 variables (s t)
40 theorem adjoin_union : adjoin R (s ∪ t) = (adjoin R s).under (adjoin (adjoin R s) t) :=
41 le_antisymm
42 (closure_mono $ set.union_subset
43 (set.range_subset_iff.2 $ λ r, or.inl ⟨algebra_map (adjoin R s) r, rfl⟩)
44 (set.union_subset_union_left _ $ λ x hxs, ⟨⟨_, subset_adjoin hxs⟩, rfl⟩))
45 (closure_subset $ set.union_subset
46 (set.range_subset_iff.2 $ λ x, adjoin_mono (set.subset_union_left _ _) x.2)
47 (set.subset.trans (set.subset_union_right _ _) subset_adjoin))
48
49 theorem adjoin_eq_span : (adjoin R s : submodule R A) = span R (monoid.closure s) :=
50 begin
51 apply le_antisymm,
src └────┘
typ └────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
52 { intros r hr, rcases ring.exists_list_of_mem_closure hr with ⟨L, HL, rfl⟩, clear hr,
src └─────────┘ └─────┘ ┴ └────────────────┘ └──────┘
typ └─────────┘ └─────┘ ┴ └────────────────┘ └──────┘
doc └─────────┘ └─────┘ ┴ └────────────────┘ └──────┘
txt └─────────┘ └─────┘ ┴ └────────────────┘ └──────┘
par └─────────┘ └─────┘ ┴ └────────────────┘ └──────┘
pid └───┘ ┴ ┴ └────────────────┘ └─┘
53 induction L with hd tl ih, { rw mem_coe, exact zero_mem _ },
id └──────┘
src └────────┘ └────────────┘ └─┘ └────┘└──────┘└─┘
typ └────────┘ └────────────┘ └─┘ └────┘└──────┘└─┘
doc └────────┘ └────────────┘ └─┘ └────┘ └─┘
txt └────────┘ └────────────┘ └─┘ └────┘ └─┘
par └────────┘ └────────────┘ └─┘ └────┘ └─┘
pid ┴ ┴└───────────┘ ┴ ┴ └┘┴
st └───────────────┘└┘└
54 rw list.forall_mem_cons at HL,
id └──────────────────┘
src └─┘└──────────────────┘└────┘
typ └─┘└──────────────────┘└────┘
doc └─┘ └────┘
txt └─┘ └────┘
par └─┘ └────┘
pid ┴ └────┘
st ────────────────────────────────┘└─
55 rw [list.map_cons, list.sum_cons, mem_coe],
id └───────────┘ └───────────┘ └─────┘
src └──┘└───────────┘└┘└───────────┘└┘└─────┘┴
typ └──┘└───────────┘└┘└───────────┘└┘└─────┘┴
doc └──┘ └┘ └┘ ┴
txt └──┘ └┘ └┘ ┴
par └──┘ └┘ └┘ ┴
pid └┘ └┘ └┘ ┴
st ────────────────────┘└─────────────┘└───────┘┴└─
56 refine submodule.add_mem _ _ (ih HL.2),
id └───────────────┘ └┘ └┘
src └─────┘└───────────────┘└───┘ ┴ └─┘
typ └─────┘└───────────────┘└───┘ └┘┴└┘└─┘
doc └─────┘ └───┘ ┴ └─┘
txt └─────┘ └───┘ ┴ └─┘
par └─────┘ └───┘ ┴ └─┘
pid ┴ └───┘ ┴ └─┘
st ─────────────────────────────────────────┘└─
57 replace HL := HL.1, clear ih tl,
id └┘
src └────────────┘ └┘ └─────────┘
typ └────────────┘└┘└┘ └─────────┘
doc └────────────┘ └┘ └─────────┘
txt └────────────┘ └┘ └─────────┘
par └────────────┘ └┘ └─────────┘
pid └─┘┴└─┘ └┘ └────┘
st ─────────────────────┘└───────────┘└─
58 suffices : ∃ z r (hr : r ∈ monoid.closure s), has_scalar.smul.{u v} z r = list.prod hd,
id ┴ ┴ └────────────┘ ┴ ┴ └─────────────┘ ┴ └───────┘ └┘
src └─────────┘┴└─────────┘ ┴┴┴└────────────┘┴ ┴┴┴└─────────────┘└─────┘ ┴ ┴┴┴└───────┘┴
typ └─────────┘┴└─────────┘ ┴┴┴└────────────┘┴┴┴┴┴└─────────────┘└─────┘ ┴ ┴┴┴└───────┘┴└┘
doc └─────────┘ └─────────┘ ┴ ┴└────────────┘┴ ┴ ┴ └─────┘ ┴ ┴ ┴└───────┘┴
txt └─────────┘ └─────────┘ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴
par └─────────┘ └─────────┘ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴
pid └───────┘└┘ └─────────┘ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴
st ─────────────────────────────────────────────────────────────────────────────────────────┘└─
59 { rcases this with ⟨z, r, hr, hzr⟩, rw ← hzr,
id └──┘ └─┘
src └─────┘ └───────────────────┘ └───┘
typ └─────┘└──┘└───────────────────┘ └───┘└─┘
doc └─────┘ └───────────────────┘ └───┘
txt └─────┘ └───────────────────┘ └───┘
par └─────┘ └───────────────────┘ └───┘
pid ┴ └───────────────────┘ └─┘
st ─────┘└──────────────────────────────┘└────────┘└─
60 exact smul_mem _ _ (subset_span hr) },
id └──────┘ └─────────┘ └┘
src └────┘└──────┘└───┘ └─────────┘┴ └┘
typ └────┘└──────┘└───┘ └─────────┘┴└┘└┘
doc └────┘ └───┘ ┴ └┘
txt └────┘ └───┘ ┴ └┘
par └────┘ └───┘ ┴ └┘
pid ┴ └───┘ ┴ ┴┴
st ─────────────────────────────────────────┘└┘└
61 induction hd with hd tl ih, { exact ⟨1, 1, is_submonoid.one_mem _, one_smul _ _⟩ },
id └┘ └──────────────────┘ └──────┘
src └────────┘ └────────────┘ └────┘ └────┘└──────────────────┘└──┘└──────┘└────┘
typ └────────┘└┘└────────────┘ └────┘ └────┘└──────────────────┘└──┘└──────┘└────┘
doc └────────┘ └────────────┘ └────┘ └────┘ └──┘ └────┘
txt └────────┘ └────────────┘ └────┘ └────┘ └──┘ └────┘
par └────────┘ └────────────┘ └────┘ └────┘ └──┘ └────┘
pid ┴ ┴└───────────┘ ┴ └────┘ └──┘ └───┘┴
st ─────────────────────────────┘└──┘└─────────────────────────────────────────────────┘└┘└
62 rw list.forall_mem_cons at HL,
id └──────────────────┘
src └─┘└──────────────────┘└────┘
typ └─┘└──────────────────┘└────┘
doc └─┘ └────┘
txt └─┘ └────┘
par └─┘ └────┘
pid ┴ └────┘
st ────────────────────────────────┘└─
63 rcases (ih HL.2) with ⟨z, r, hr, hzr⟩, rw [list.prod_cons, ← hzr],
id └┘ └┘ └────────────┘ └─┘
src └─────┘ ┴ └──────────────────────┘ └──┘└────────────┘└──┘ ┴
typ └─────┘ └┘┴└┘└──────────────────────┘ └──┘└────────────┘└──┘└─┘┴
doc └─────┘ ┴ └──────────────────────┘ └──┘ └──┘ ┴
txt └─────┘ ┴ └──────────────────────┘ └──┘ └──┘ ┴
par └─────┘ ┴ └──────────────────────┘ └──┘ └──┘ ┴
pid ┴ ┴ └──────────────────────┘ └┘ └──┘ ┴
st ────────────────────────────────────────┘└──────────────────┘└─────┘└──
64 rcases HL.1 with ⟨⟨hd, rfl⟩ | hs⟩ | rfl,
id └┘
src └─────┘ └────────────────────────────┘
typ └─────┘└┘└────────────────────────────┘
doc └─────┘ └────────────────────────────┘
txt └─────┘ └────────────────────────────┘
par └─────┘ └────────────────────────────┘
pid ┴ └────────────────────────────┘
st ──────────────────────────────────────────┘└─
65 { refine ⟨hd * z, r, hr, _⟩, rw [smul_def, smul_def, map_mul, ring.mul_assoc], refl },
id └┘ ┴ ┴ ┴ └┘ └──────┘ └──────┘ └─────┘ └────────────┘
src └─────┘ ┴┴┴ └┘ └┘ └──┘ └──┘└──────┘└┘└──────┘└┘└─────┘└┘└────────────┘┴ └───┘
typ └─────┘ └┘┴┴┴┴└┘┴└┘└┘└──┘ └──┘└──────┘└┘└──────┘└┘└─────┘└┘└────────────┘┴ └───┘
doc └─────┘ ┴ ┴ └┘ └┘ └──┘ └──┘ └┘ └┘ └┘ ┴ └───┘
txt └─────┘ ┴ ┴ └┘ └┘ └──┘ └──┘ └┘ └┘ └┘ ┴ └───┘
par └─────┘ ┴ ┴ └┘ └┘ └──┘ └──┘ └┘ └┘ └┘ ┴ └───┘
pid ┴ ┴ ┴ └┘ └┘ └──┘ └┘ └┘ └┘ └┘ ┴ ┴
st ─────┘└───────────────────────┘└────────────┘└────────┘└───────┘└──────────────┘└──────┘└┘└
66 { refine ⟨z, hd * r, is_submonoid.mul_mem (monoid.subset_closure hs) hr, _⟩,
id ┴ └┘ ┴ └──────────────────┘ └───────────────────┘ └┘ └┘
src └─────┘ └┘ ┴ ┴ └┘└──────────────────┘┴ └───────────────────┘┴ └┘ └──┘
typ └─────┘ ┴└┘└┘┴ ┴┴└┘└──────────────────┘┴ └───────────────────┘┴└┘└┘└┘└──┘
doc └─────┘ └┘ ┴ ┴ └┘ ┴ └───────────────────┘┴ └┘ └──┘
txt └─────┘ └┘ ┴ ┴ └┘ ┴ ┴ └┘ └──┘
par └─────┘ └┘ ┴ ┴ └┘ ┴ ┴ └┘ └──┘
pid ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ └──┘
st ─────┘└───────────────────────────────────────────────────────────────────────┘└─
67 rw [smul_def, smul_def, mul_left_comm] },
id └──────┘ └──────┘ └───────────┘
src └──┘└──────┘└┘└──────┘└┘└───────────┘└┘
typ └──┘└──────┘└┘└──────┘└┘└───────────┘└┘
doc └──┘ └┘ └┘ └┘
txt └──┘ └┘ └┘ └┘
par └──┘ └┘ └┘ └┘
pid └┘ └┘ └┘ ┴┴
st ─────────────────┘└────────┘└─────────────┘┴┴└┘└
68 { refine ⟨-z, r, hr, _⟩, rw [neg_smul, neg_one_mul] } },
id ┴┴ ┴ └┘ └──────┘ └─────────┘
src └─────┘ ┴ └┘ └┘ └──┘ └──┘└──────┘└┘└─────────┘└┘
typ └─────┘ ┴┴└┘┴└┘└┘└──┘ └──┘└──────┘└┘└─────────┘└┘
doc └─────┘ └┘ └┘ └──┘ └──┘ └┘└─────────┘└┘
txt └─────┘ └┘ └┘ └──┘ └──┘ └┘ └┘
par └─────┘ └┘ └┘ └──┘ └──┘ └┘ └┘
pid ┴ └┘ └┘ └──┘ └┘ └┘ ┴┴
st ──────────────────────────┘└────────────┘└───────────┘┴┴└──┘└
69 exact span_le.2 (show monoid.closure s ⊆ adjoin R s, from monoid.closure_subset subset_adjoin)
id └─────┘ └────────────┘ ┴ └────┘ ┴ ┴ └───────────────────┘ └───────────┘
src └────┘└─────┘└─┘ ┴└────────────┘┴ ┴┴┴└────┘┴ ┴ └─────┘└───────────────────┘┴└───────────┘└┘
typ └────┘└─────┘└─┘ ┴└────────────┘┴ ┴┴┴└────┘┴┴┴┴└─────┘└───────────────────┘┴└───────────┘└┘
doc └────┘ └─┘ ┴└────────────┘┴ ┴ ┴ ┴ ┴ └─────┘└───────────────────┘┴ └┘
txt └────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ └┘
par └────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ └┘
pid ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴┴
st ────────────────────────────────────────────────────────────────────────────────────────────────┘
70 end
st └─┘
71
72 theorem adjoin_eq_range [decidable_eq R] [decidable_eq A] :
id └──────────┘ ┴ └──────────┘ ┴
src └──────────┘ └──────────┘
typ └──────────┘ ┴ └──────────┘ ┴
73 adjoin R s = (mv_polynomial.aeval R A s).range :=
id └────┘ ┴ ┴ ┴ └─────────────────┘ ┴ ┴ ┴ └───┘
src └────┘ ┴ └─────────────────┘ └───┘
typ └────┘ ┴ ┴ ┴ └─────────────────┘ ┴ ┴ ┴ └───┘
doc └─────────────────┘
74 le_antisymm
id └─────────┘
src └─────────┘
typ └─────────┘
75 (adjoin_le $ λ x hx, ⟨mv_polynomial.X ⟨x, hx⟩, mv_polynomial.eval₂_X _ _ _⟩)
id └───────┘ ┴ └┘ └─────────────┘ ┴ └┘ └───────────────────┘
src └───────┘ └─────────────┘ └───────────────────┘
typ └───────┘ ┴ └┘ └─────────────┘ ┴ └┘ └───────────────────┘
doc └─────────────┘
76 (λ x ⟨p, hp⟩, hp ▸ mv_polynomial.induction_on p
id ┴ ┴┴ └┘ ┴ └────────────────────────┘
src ┴ └────────────────────────┘
typ ┴ ┴┴ └┘ ┴ └────────────────────────┘
77 (λ r, by rw [mv_polynomial.aeval_def, mv_polynomial.eval₂_C]; exact (adjoin R s).3 ⟨r, rfl⟩)
id ┴ └─────────────────────┘ └───────────────────┘ └────┘ ┴ ┴ ┴ └─┘
src └──┘└─────────────────────┘└┘└───────────────────┘┴ └────┘ └────┘┴ ┴ └──┘ └┘└─┘┴
typ ┴ └──┘└─────────────────────┘└┘└───────────────────┘┴ └────┘ └────┘┴┴┴┴└──┘ ┴└┘└─┘┴
doc └──┘ └┘ ┴ └────┘ ┴ ┴ └──┘ └┘ ┴
txt └──┘ └┘ ┴ └────┘ ┴ ┴ └──┘ └┘ ┴
par └──┘ └┘ ┴ └────┘ ┴ ┴ └──┘ └┘ ┴
pid └┘ └┘ ┴ ┴ ┴ ┴ └──┘ └┘ ┴
st └──────────────────────────┘└─────────────────────┘┴└─────────────────────────────┘
78 (λ p q hp hq, by rw alg_hom.map_add; exact is_add_submonoid.add_mem hp hq)
id ┴ ┴ └┘ └┘ └─────────────┘ └──────────────────────┘ └┘ └┘
src └─┘└─────────────┘ └────┘└──────────────────────┘┴ ┴
typ ┴ ┴ └┘ └┘ └─┘└─────────────┘ └────┘└──────────────────────┘┴└┘┴└┘
doc └─┘ └────┘ ┴ ┴
txt └─┘ └────┘ ┴ ┴
par └─┘ └────┘ ┴ ┴
pid ┴ ┴ ┴ ┴
st └───────────────────────────────────────────────────────┘
79 (λ p ⟨n, hn⟩ hp, by rw [alg_hom.map_mul, mv_polynomial.aeval_def _ _ _ (mv_polynomial.X _),
id ┴ ┴ └┘ └─────────────┘ └─────────────────────┘ └─────────────┘
src └──┘└─────────────┘└┘└─────────────────────┘└─────┘ └─────────────┘└────
typ ┴ ┴ └┘ └──┘└─────────────┘└┘└─────────────────────┘└─────┘ └─────────────┘└────
doc └──┘ └┘ └─────┘ └─────────────┘└────
txt └──┘ └┘ └─────┘ └────
par └──┘ └┘ └─────┘ └────
pid └┘ └┘ └─────┘ └────
st └──────────────────┘└─────────────────────────────────────────────────┘└─
80 mv_polynomial.eval₂_X]; exact is_submonoid.mul_mem hp (subset_adjoin hn)))
id └───────────────────┘ └──────────────────┘ └┘ └───────────┘ └┘
src ─────┘└───────────────────┘┴ └────┘└──────────────────┘┴ ┴ └───────────┘┴ ┴
typ ─────┘└───────────────────┘┴ └────┘└──────────────────┘┴└┘┴ └───────────┘┴└┘┴
doc ─────┘ ┴ └────┘ ┴ ┴ ┴ ┴
txt ─────┘ ┴ └────┘ ┴ ┴ ┴ ┴
par ─────┘ ┴ └────┘ ┴ ┴ ┴ ┴
pid ─────┘ ┴ ┴ ┴ ┴ ┴ ┴
st ──────────────────────────┘┴└────────────────────────────────────────────────┘
81
82 theorem adjoin_singleton_eq_range [decidable_eq R] [decidable_eq A] (x : A) :
id └──────────┘ ┴ └──────────┘ ┴ ┴
src └──────────┘ └──────────┘
typ └──────────┘ ┴ └──────────┘ ┴ ┴
83 adjoin R {x} = (polynomial.aeval R A x).range :=
id └────┘ ┴ ┴┴ ┴ └──────────────┘ ┴ ┴ ┴ └───┘
src └────┘ ┴ ┴ └──────────────┘ └───┘
typ └────┘ ┴ ┴┴ ┴ └──────────────┘ ┴ ┴ ┴ └───┘
doc └──────────────┘
84 le_antisymm
id └─────────┘
src └─────────┘
typ └─────────┘
85 (adjoin_le $ set.singleton_subset_iff.2 ⟨polynomial.X, polynomial.eval₂_X _ _⟩)
id └───────┘ └──────────────────────┘┴ └──────────┘ └────────────────┘
src └───────┘ └──────────────────────┘┴ └──────────┘ └────────────────┘
typ └───────┘ └──────────────────────┘┴ └──────────┘ └────────────────┘
doc └──────────┘
86 (λ y ⟨p, hp⟩, hp ▸ polynomial.induction_on p
id ┴ ┴┴ └┘ ┴ └─────────────────────┘
src ┴ └─────────────────────┘
typ ┴ ┴┴ └┘ ┴ └─────────────────────┘
87 (λ r, by rw [polynomial.aeval_def, polynomial.eval₂_C]; exact (adjoin R _).3 ⟨r, rfl⟩)
id ┴ └──────────────────┘ └────────────────┘ └────┘ ┴ ┴ └─┘
src └──┘└──────────────────┘└┘└────────────────┘┴ └────┘ └────┘┴ └────┘ └┘└─┘┴
typ ┴ └──┘└──────────────────┘└┘└────────────────┘┴ └────┘ └────┘┴┴└────┘ ┴└┘└─┘┴
doc └──┘ └┘ ┴ └────┘ ┴ └────┘ └┘ ┴
txt └──┘ └┘ ┴ └────┘ ┴ └────┘ └┘ ┴
par └──┘ └┘ ┴ └────┘ ┴ └────┘ └┘ ┴
pid └┘ └┘ ┴ ┴ ┴ └────┘ └┘ ┴
st └───────────────────────┘└──────────────────┘┴└─────────────────────────────┘
88 (λ p q hp hq, by rw alg_hom.map_add; exact is_add_submonoid.add_mem hp hq)
id ┴ ┴ └┘ └┘ └─────────────┘ └──────────────────────┘ └┘ └┘
src └─┘└─────────────┘ └────┘└──────────────────────┘┴ ┴
typ ┴ ┴ └┘ └┘ └─┘└─────────────┘ └────┘└──────────────────────┘┴└┘┴└┘
doc └─┘ └────┘ ┴ ┴
txt └─┘ └────┘ ┴ ┴
par └─┘ └────┘ ┴ ┴
pid ┴ ┴ ┴ ┴
st └───────────────────────────────────────────────────────┘
89 (λ n r ih, by rw [pow_succ', ← ring.mul_assoc, alg_hom.map_mul, polynomial.aeval_def _ _ _ polynomial.X,
id ┴ ┴ └┘ └───────┘ └────────────┘ └─────────────┘ └──────────────────┘ └──────────┘
src └──┘└───────┘└──┘└────────────┘└┘└─────────────┘└┘└──────────────────┘└─────┘└──────────┘└─
typ ┴ ┴ └┘ └──┘└───────┘└──┘└────────────┘└┘└─────────────┘└┘└──────────────────┘└─────┘└──────────┘└─
doc └──┘ └──┘ └┘ └┘ └─────┘└──────────┘└─
txt └──┘ └──┘ └┘ └┘ └─────┘ └─
par └──┘ └──┘ └┘ └┘ └─────┘ └─
pid └┘ └──┘ └┘ └┘ └─────┘ └─
st └────────────┘└────────────────┘└───────────────┘└───────────────────────────────────────┘└─
90 polynomial.eval₂_X]; exact is_submonoid.mul_mem ih (subset_adjoin $ or.inl rfl)))
id └────────────────┘ └──────────────────┘ └┘ └───────────┘ └────┘ └─┘
src ─────┘└────────────────┘┴ └────┘└──────────────────┘┴ ┴ └───────────┘┴ ┴└────┘┴└─┘┴
typ ─────┘└────────────────┘┴ └────┘└──────────────────┘┴└┘┴ └───────────┘┴ ┴└────┘┴└─┘┴
doc ─────┘ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴
txt ─────┘ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴
par ─────┘ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴
pid ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ───────────────────────┘┴└──────────────────────────────────────────────────────────┘
91
92 theorem adjoin_union_coe_submodule : (adjoin R (s ∪ t) : submodule R A) =
id └────┘ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴
src └────┘ ┴ └───────┘ ┴
typ └────┘ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴
doc └───────┘
93 (adjoin R s) * (adjoin R t) :=
id └────┘ ┴ ┴ ┴ └────┘ ┴ ┴
src └────┘ ┴ └────┘
typ └────┘ ┴ ┴ ┴ └────┘ ┴ ┴
94 begin
st └─────
95 rw [adjoin_eq_span, adjoin_eq_span, adjoin_eq_span, span_mul_span],
id └────────────┘ └────────────┘ └────────────┘ └───────────┘
src └──┘└────────────┘└┘└────────────┘└┘└────────────┘└┘└───────────┘┴
typ └──┘└────────────┘└┘└────────────┘└┘└────────────┘└┘└───────────┘┴
doc └──┘ └┘ └┘ └┘ ┴
txt └──┘ └┘ └┘ └┘ ┴
par └──┘ └┘ └┘ └┘ ┴
pid └┘ └┘ └┘ └┘ ┴
st ───────────────────┘└──────────────┘└──────────────┘└─────────────┘└──
96 congr' 1,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid ┴┴
st ─────────┘└─
97 ext z,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid └┘
st ──────┘└─
98 rw monoid.mem_closure_union_iff,
id └──────────────────────────┘
src └─┘└──────────────────────────┘
typ └─┘└──────────────────────────┘
doc └─┘└──────────────────────────┘
txt └─┘
par └─┘
pid ┴
st ────────────────────────────────┘└─
99 split;
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ─────────
100 { rintro ⟨y, hys, z, hzt, rfl⟩, exact ⟨_, hys, _, hzt, rfl⟩ }
id └─┘ └─┘ └─┘
src └──────────────────────────┘ └────┘ └─┘ └───┘ └┘└─┘└┘
typ └──────────────────────────┘ └────┘ └─┘└─┘└───┘└─┘└┘└─┘└┘
doc └──────────────────────────┘ └────┘ └─┘ └───┘ └┘ └┘
txt └──────────────────────────┘ └────┘ └─┘ └───┘ └┘ └┘
par └──────────────────────────┘ └────┘ └─┘ └───┘ └┘ └┘
pid └────────────────────┘ ┴ └─┘ └───┘ └┘ ┴┴
st ─┘└────────────────────────────┘└────────────────────────────┘└─
101 end
st ──┘
102 variables {R s t}
103
104 theorem adjoin_int (s : set R) : adjoin ℤ s = subalgebra_of_subring (ring.closure s) :=
id └─┘ ┴ └────┘ ┴ ┴ ┴ └───────────────────┘ └──────────┘ ┴
src └─┘ └────┘ ┴ ┴ └───────────────────┘ └──────────┘
typ └─┘ ┴ └────┘ ┴ ┴ ┴ └───────────────────┘ └──────────┘ ┴
doc └───────────────────┘
st ┴
105 le_antisymm (adjoin_le subset_closure) (closure_subset subset_adjoin)
id └─────────┘ └───────┘ └────────────┘ └────────────┘ └───────────┘
src └─────────┘ └───────┘ └────────────┘ └────────────┘ └───────────┘
typ └─────────┘ └───────┘ └────────────┘ └────────────┘ └───────────┘
106
107 local attribute [instance] set.pointwise_mul_semiring
id └────────────────────────┘
src └────────────────────────┘
typ └────────────────────────┘
108
109 theorem fg_trans (h1 : (adjoin R s : submodule R A).fg)
id └────┘ ┴ ┴ └───────┘ ┴ ┴ └┘
src └────┘ └───────┘ └┘
typ └────┘ ┴ ┴ └───────┘ ┴ ┴ └┘
doc └───────┘
110 (h2 : (adjoin (adjoin R s) t : submodule (adjoin R s) A).fg) :
id └────┘ └────┘ ┴ ┴ ┴ └───────┘ └────┘ ┴ ┴ ┴ └┘
src └────┘ └────┘ └───────┘ └────┘ └┘
typ └────┘ └────┘ ┴ ┴ ┴ └───────┘ └────┘ ┴ ┴ ┴ └┘
doc └───────┘
111 (adjoin R (s ∪ t) : submodule R A).fg :=
id └────┘ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ └┘
src └────┘ ┴ └───────┘ └┘
typ └────┘ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ └┘
doc └───────┘
112 begin
st └─────
113 rcases fg_def.1 h1 with ⟨p, hp, hp'⟩,
id └────┘ └┘
src └─────┘└────┘└─┘ └────────────────┘
typ └─────┘└────┘└─┘└┘└────────────────┘
doc └─────┘ └─┘ └────────────────┘
txt └─────┘ └─┘ └────────────────┘
par └─────┘ └─┘ └────────────────┘
pid ┴ └─┘ └────────────────┘
st ─────────────────────────────────────┘└─
114 rcases fg_def.1 h2 with ⟨q, hq, hq'⟩,
id └────┘ └┘
src └─────┘└────┘└─┘ └────────────────┘
typ └─────┘└────┘└─┘└┘└────────────────┘
doc └─────┘ └─┘ └────────────────┘
txt └─────┘ └─┘ └────────────────┘
par └─────┘ └─┘ └────────────────┘
pid ┴ └─┘ └────────────────┘
st ─────────────────────────────────────┘└─
115 refine fg_def.2 ⟨p * q, set.pointwise_mul_finite hp hq, le_antisymm _ _⟩,
id └────┘ ┴ ┴ ┴ └──────────────────────┘ └┘ └┘ └─────────┘
src └─────┘└────┘└─┘ ┴┴┴ └┘└──────────────────────┘┴ ┴ └┘└─────────┘└───┘
typ └─────┘└────┘└─┘ ┴┴┴┴┴└┘└──────────────────────┘┴└┘┴└┘└┘└─────────┘└───┘
doc └─────┘ └─┘ ┴ ┴ └┘ ┴ ┴ └┘ └───┘
txt └─────┘ └─┘ ┴ ┴ └┘ ┴ ┴ └┘ └───┘
par └─────┘ └─┘ ┴ ┴ └┘ ┴ ┴ └┘ └───┘
pid ┴ └─┘ ┴ ┴ └┘ ┴ ┴ └┘ └───┘
st ─────────────────────────────────────────────────────────────────────────┘└─
116 { rw [span_le],
id └─────┘
src └──┘└─────┘┴
typ └──┘└─────┘┴
doc └──┘ ┴
txt └──┘ ┴
par └──┘ ┴
pid └┘ ┴
st ───┘└─────────┘└──
117 rintros _ ⟨x, hx, y, hy, rfl⟩,
src └───────────────────────────┘
typ └───────────────────────────┘
doc └───────────────────────────┘
txt └───────────────────────────┘
par └───────────────────────────┘
pid └────────────────────┘
st ────────────────────────────────┘└─
118 change x * y ∈ _,
id ┴ ┴ ┴
src └─────┘ ┴ ┴ ┴┴└┘
typ └─────┘┴┴ ┴┴┴┴└┘
doc └─────┘ ┴ ┴ ┴ └┘
txt └─────┘ ┴ ┴ ┴ └┘
par └─────┘ ┴ ┴ ┴ └┘
pid ┴ ┴ ┴ ┴ └┘
st ───────────────────┘└─
119 refine is_submonoid.mul_mem _ _,
id └──────────────────┘
src └─────┘└──────────────────┘└──┘
typ └─────┘└──────────────────┘└──┘
doc └─────┘ └──┘
txt └─────┘ └──┘
par └─────┘ └──┘
pid ┴ └──┘
st ──────────────────────────────────┘└─
120 { have : x ∈ (adjoin R s : submodule R A),
id ┴ └────┘ ┴ ┴ └───────┘ ┴
src └─────┘ ┴ ┴ └────┘┴ ┴ └─┘└───────┘┴ ┴ ┴
typ └─────┘┴┴ ┴ └────┘┴┴┴┴└─┘└───────┘┴ ┴┴┴
doc └─────┘ ┴ ┴ ┴ ┴ └─┘└───────┘┴ ┴ ┴
txt └─────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴
par └─────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴
pid └───┘└┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴
st ─────┘└─────────────────────────────────────┘└─
121 { rw ← hp', exact subset_span hx },
id └─┘ └─────────┘ └┘
src └───┘ └────┘└─────────┘┴ ┴
typ └───┘└─┘ └────┘└─────────┘┴└┘┴
doc └───┘ └────┘ ┴ ┴
txt └───┘ └────┘ ┴ ┴
par └───┘ └────┘ ┴ ┴
pid └─┘ ┴ ┴ ┴
st ───────┘└──────┘└─────────────────────┘└┘└
122 exact adjoin_mono (set.subset_union_left _ _) this },
id └─────────┘ └───────────────────┘ └──┘
src └────┘└─────────┘┴ └───────────────────┘└────┘ ┴
typ └────┘└─────────┘┴ └───────────────────┘└────┘└──┘┴
doc └────┘ ┴ └────┘ ┴
txt └────┘ ┴ └────┘ ┴
par └────┘ ┴ └────┘ ┴
pid ┴ ┴ └────┘ ┴
st ────────────────────────────────────────────────────────┘└┘└
123 have : y ∈ (adjoin (adjoin R s) t : submodule (adjoin R s) A),
id ┴ └────┘ ┴ ┴ ┴ └───────┘ ┴
src └─────┘ ┴ ┴ ┴ └────┘┴ ┴ └┘ └─┘└───────┘┴ ┴ ┴ └┘ ┴
typ └─────┘┴┴ ┴ ┴ └────┘┴┴┴┴└┘┴└─┘└───────┘┴ ┴ ┴ └┘┴┴
doc └─────┘ ┴ ┴ ┴ ┴ ┴ └┘ └─┘└───────┘┴ ┴ ┴ └┘ ┴
txt └─────┘ ┴ ┴ ┴ ┴ ┴ └┘ └─┘ ┴ ┴ ┴ └┘ ┴
par └─────┘ ┴ ┴ ┴ ┴ ┴ └┘ └─┘ ┴ ┴ ┴ └┘ ┴
pid └───┘└┘ ┴ ┴ ┴ ┴ ┴ └┘ └─┘ ┴ ┴ ┴ └┘ ┴
st ────────────────────────────────────────────────────────────────┘└─
124 { rw ← hq', exact subset_span hy },
id └─┘ └─────────┘ └┘
src └───┘ └────┘└─────────┘┴ ┴
typ └───┘└─┘ └────┘└─────────┘┴└┘┴
doc └───┘ └────┘ ┴ ┴
txt └───┘ └────┘ ┴ ┴
par └───┘ └────┘ ┴ ┴
pid └─┘ ┴ ┴ ┴
st ────┘ └──────┘└─────────────────────┘┴ └
125 change y ∈ adjoin R (s ∪ t), rwa adjoin_union },
id ┴ └────┘ ┴ ┴ ┴ ┴
src └─────┘ ┴ ┴└────┘┴ ┴ ┴┴┴ ┴
typ └─────┘┴┴ ┴└────┘┴┴┴ ┴┴┴┴┴┴
doc └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
txt └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ──────────────────────────────┘ ┴
126 { intros r hr,
127 change r ∈ adjoin R (s ∪ t) at hr,
128 rw adjoin_union at hr,
129 change r ∈ (adjoin (adjoin R s) t : submodule (adjoin R s) A) at hr,
130 haveI := classical.dec_eq A,
131 haveI := classical.dec_eq R,
132 rw [← hq', ← set.image_id q, finsupp.mem_span_iff_total (adjoin R s)] at hr,
133 rcases hr with ⟨l, hlq, rfl⟩,
134 have := @finsupp.total_apply A A (adjoin R s),
135 rw [this, finsupp.sum, mem_coe],
136 refine sum_mem _ _,
137 intros z hz, change (l z).1 * _ ∈ _,
138 have : (l z).1 ∈ (adjoin R s : submodule R A) := (l z).2,
139 rw [← hp', ← set.image_id p, finsupp.mem_span_iff_total R] at this,
140 rcases this with ⟨l2, hlp, hl⟩,
141 have := @finsupp.total_apply A A R,
142 rw this at hl,
143 rw [←hl, finsupp.sum_mul],
144 refine sum_mem _ _,
145 intros t ht, change _ * _ ∈ _, rw smul_mul_assoc, refine smul_mem _ _ _,
146 exact subset_span ⟨t, hlp ht, z, hlq hz, rfl⟩ }
st └─
147 end
st ──┘
148
149 end algebra
150
151 namespace subalgebra
152
153 variables {R : Type u} {A : Type v}
154 variables [comm_ring R] [comm_ring A] [algebra R A]
id └───────┘ └───────┘ └─────┘
src └───────┘ └───────┘ └─────┘
typ └───────┘ └───────┘ └─────┘
doc └─────┘
155
156 def fg (S : subalgebra R A) : Prop :=
id └────────┘ ┴ ┴
src └────────┘
typ └────────┘ ┴ ┴
157 ∃ t : finset A, algebra.adjoin R ↑t = S
id ┴ └────┘ ┴┴ └────────────┘ ┴ ┴┴ ┴ ┴
src ┴ └────┘ ┴ └────────────┘ ┴ ┴
typ ┴ └────┘ ┴┴ └────────────┘ ┴ ┴┴ ┴ ┴
doc └────┘
158
159 theorem fg_def {S : subalgebra R A} : S.fg ↔ ∃ t : set A, set.finite t ∧ algebra.adjoin R t = S :=
id └────────┘ ┴ ┴ ┴└─┘ ┴ ┴ └─┘ ┴┴ └────────┘ ┴ ┴ └────────────┘ ┴ ┴ ┴ ┴
src └────────┘ └─┘ ┴ ┴ └─┘ ┴ └────────┘ ┴ └────────────┘ ┴
typ └────────┘ ┴ ┴ ┴└─┘ ┴ ┴ └─┘ ┴┴ └────────┘ ┴ ┴ └────────────┘ ┴ ┴ ┴ ┴
doc └────────┘
160 ⟨λ ⟨t, ht⟩, ⟨↑t, set.finite_mem_finset t, ht⟩,
id ┴┴ └┘ ┴ └───────────────────┘
src ┴ └───────────────────┘
typ ┴┴ └┘ ┴ └───────────────────┘
161 λ ⟨t, ht1, ht2⟩, ⟨ht1.to_finset, by rwa finset.coe_to_finset⟩⟩
id ┴ └─┘ └────────┘ └──────────────────┘
src └────────┘ └──┘└──────────────────┘
typ ┴ └─┘ └────────┘ └──┘└──────────────────┘
doc └────────┘ └──┘
txt └──┘
par └──┘
pid ┴
st └───────────────────────┘
162
163 theorem fg_bot : (⊥ : subalgebra R A).fg :=
id ┴ └────────┘ ┴ ┴ └┘
src ┴ └────────┘ └┘
typ ┴ └────────┘ ┴ ┴ └┘
164 ⟨∅, algebra.adjoin_empty R A⟩
id ┴ └──────────────────┘ ┴ ┴
src ┴ └──────────────────┘
typ ┴ └──────────────────┘ ┴ ┴
165
166 end subalgebra
167
168 variables {R : Type u} {A : Type v} {B : Type w}
169 variables [comm_ring R] [comm_ring A] [comm_ring B] [algebra R A] [algebra R B]
id └───────┘ └───────┘ └───────┘ └─────┘ └─────┘
src └───────┘ └───────┘ └───────┘ └─────┘ └─────┘
typ └───────┘ └───────┘ └───────┘ └─────┘ └─────┘
doc └─────┘ └─────┘
170
171 instance alg_hom.is_noetherian_ring_range (f : A →ₐ[R] B) [is_noetherian_ring A] :
id ┴ └─┘┴┴ ┴ └────────────────┘ ┴
src └─┘ ┴ └────────────────┘
typ ┴ └─┘┴┴ ┴ └────────────────┘ ┴
doc └─┘ ┴
172 is_noetherian_ring f.range :=
id └────────────────┘ ┴└────┘
src └────────────────┘ └────┘
typ └────────────────┘ ┴└────┘
173 is_noetherian_ring_range f
id └──────────────────────┘ ┴
src └──────────────────────┘
typ └──────────────────────┘ ┴
174
175 variables [decidable_eq R] [decidable_eq A]
id └──────────┘ └──────────┘
src └──────────┘ └──────────┘
typ └──────────┘ └──────────┘
176
177 theorem is_noetherian_ring_of_fg {S : subalgebra R A} (HS : S.fg)
id └────────┘ ┴ ┴ ┴└─┘
src └────────┘ └─┘
typ └────────┘ ┴ ┴ ┴└─┘
178 [is_noetherian_ring R] : is_noetherian_ring S :=
id └────────────────┘ ┴ └────────────────┘ ┴
src └────────────────┘ └────────────────┘
typ └────────────────┘ ┴ └────────────────┘ ┴
179 let ⟨t, ht⟩ := HS in ht ▸ (algebra.adjoin_eq_range R (↑t : set A)).symm ▸
id └─┘ ┴ └┘ └┘ ┴ └─────────────────────┘ ┴ ┴ └─┘ ┴ └──┘ ┴
src ┴ └─────────────────────┘ ┴ └─┘ └──┘ ┴
typ └─┘ ┴ └┘ └┘ ┴ └─────────────────────┘ ┴ ┴ └─┘ ┴ └──┘ ┴
180 by haveI : is_noetherian_ring (mv_polynomial (↑t : set A) R) :=
id └────────────────┘ └───────────┘ ┴┴ └─┘ ┴ ┴
src └──────┘└────────────────┘┴ └───────────┘┴ ┴ └─┘└─┘┴ └┘ └───┘
typ └──────┘└────────────────┘┴ └───────────┘┴ ┴┴└─┘└─┘┴┴└┘┴└───┘
doc └──────┘ ┴ └───────────┘┴ └─┘ ┴ └┘ └───┘
txt └──────┘ ┴ ┴ └─┘ ┴ └┘ └───┘
par └──────┘ ┴ ┴ └─┘ ┴ └┘ └───┘
pid ┴└┘ ┴ ┴ └─┘ ┴ └┘ ┴└──┘
st └─────────────────────────────────────────────────────────────
181 is_noetherian_ring_mv_polynomial_of_fintype;
id └─────────────────────────────────────────┘
src └─────────────────────────────────────────┘
typ └─────────────────────────────────────────┘
st ─────────────────────────────────────────────
182 convert alg_hom.is_noetherian_ring_range _; apply_instance
id └──────────────────────────────┘
src └──────┘└──────────────────────────────┘└┘ └──────────────
typ └──────┘└──────────────────────────────┘└┘ └──────────────
doc └──────┘ └┘ └──────────────
txt └──────┘ └┘ └──────────────
par └──────┘ └┘ └──────────────
pid ┴ └┘ └
st ───────────────────────────────────────────────────────────
183
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
184 theorem is_noetherian_ring_closure (s : set R) (hs : s.finite) :
id └─┘ ┴ ┴└─────┘
src └─┘ └─────┘
typ └─┘ ┴ ┴└─────┘
doc └─────┘
185 is_noetherian_ring (ring.closure s) :=
id └────────────────┘ └──────────┘ ┴
src └────────────────┘ └──────────┘
typ └────────────────┘ └──────────┘ ┴
186 show is_noetherian_ring (subalgebra_of_subring (ring.closure s)), from
id └────────────────┘ └───────────────────┘ └──────────┘ ┴
src └────────────────┘ └───────────────────┘ └──────────┘
typ └────────────────┘ └───────────────────┘ └──────────┘ ┴
doc └───────────────────┘
187 algebra.adjoin_int s ▸ is_noetherian_ring_of_fg (subalgebra.fg_def.2 ⟨s, hs, rfl⟩)
id └────────────────┘ ┴ ┴ └──────────────────────┘ └───────────────┘┴ ┴ └┘ └─┘
src └────────────────┘ ┴ └──────────────────────┘ └───────────────┘┴ └─┘
typ └────────────────┘ ┴ ┴ └──────────────────────┘ └───────────────┘┴ ┴ └┘ └─┘